basic constructions:
strong axioms
further
There are a number of ways to present a set theory; one of the most basic decisions when it comes to presenting a set theory is whether the probable sets and probable elements should be regarded as the same kind of objects, as in unsorted set theory, or as fundamentally different objects, as in two-sorted set theory or three-sorted set theory. In the former, there is a global membership relation which is defined on the entire domain of discourse. In the latter, there are two domains of discourse, one representing the probable sets and the other representing the probable elements or atoms, and for the membership relation , is required to be a probable element and is required to be a probable set.
Furthermore, in an unsorted set theory, there is also a global equality predicate, whereby it is meaningful to ask, given any two objects, whether those two objects are equal. Additionally, a set’s identity here is determined by its elements, in other words the axiom of weak extensionality holds for the global membership relation with respect to the equality relation.
Unsorted set theories come in both material set theory and structural set theory flavors. For example, ZFC, ZFA, and New Foundations are unsorted material set theories, while fully formal ETCS is an unsorted structural set theory.
First of all, in order to give a definition pertaining to all unsorted set theories, we need to know: what is a set theory? Probably no theory can intrinsically be called a set theory; it is only given that distinction by our intent to regard some of its objects of study as “sets” and others as their “elements.” Thus we make the following definition.
A notion of set and element in a unsorted first-order theory consists of:
A binary predicate called equality
A unary predicate called being a set
A unary predicate called being an element
A binary predicate called membership
such that
In pure set theories, such as ZFC and New Foundations, and is for all objects , is the primitive membership relation and is defined through the axiom of extensionality.
In set theories with urelements, such as ZFA, only is for all objects , is the primitive membership relation, is the primitive sethood predicate, and is defined through the axiom of extensionality.
In an unsorted categorical set theory, such as Todd Trimble‘s fully formal ETCS, is a primitive, and there is a specified symbol representing the identity morphism of the terminal object and a specified symbol representing the identity morphism of the initial object, as well as and representing the identity morphisms of the source and target. The elements are functions with domain , There are many possible notions of sets, three of which include:
sets as identity functions or
sets as functions out of the empty set ().
Thus, there are many different definitions of the membership relation , which for the above notions of set are:
for sets as identity functions, the membership relation is defined as
for sets as functions into the singleton, the membership relation is defined as
for sets as functions out of the empty set, the membership relation is defined as
For the first two membership relations , the singleton is a Quine atom, and any set in bijection with is a Quine atom. For the third membership relation, there are no Quine atoms. While all the membership relations defined above are weakly extensional relations, all three membership relations defined above could be proven not to be strongly extensional relations, which means that the axiom of foundation fails in any of the three unsorted presentations of categorical set theory.
Last revised on November 17, 2022 at 15:15:35. See the history of this page for a list of all contributions to it.